Lean勉強会 2023-11-19
第一回
ProofWidgets4
の
コードリーディング
ProofWidgets4/ProofWidgets/Demos/Graphics2D.lean at v0.0.3
『An Extensible User Interface for Lean 4』
ProofWidgets/Demos/Graphics2D.lean at v0.0.3
https://github.com/leanprover-community/ProofWidgets4/blob/v0.0.3/ProofWidgets/Demos/Graphics2D.lean
#L91
Id.run
lean4/src/Init/Control/Id.lean#L27
恒等モナド
ルービックキューブ
widget/src/rubiks.tsx at v0.0.3
https://github.com/leanprover-community/ProofWidgets4/blob/v0.0.3/widget/src/rubiks.tsx
ProofWidgets/Demos/Rubiks.lean at v0.0.3
https://github.com/leanprover-community/ProofWidgets4/blob/v0.0.3/ProofWidgets/Demos/Rubiks.lean
React
、
TypeScript
で作られているっぽい
ルービックキューブを表示する
ウィジェットのマニュアル:
User Widgets - Lean Manual
ルービックキューブの実装例(Elm)
Elm でつくるルービックキューブ - Speaker Deck
Main
ブラウザ上で動くルービックキューブを Elm で作った
elaboratione
英語「elaboration」の意味・使い方・読み方 | Weblio英和辞書
elabolator
Elaboratorリフレクションでメタプログラミング｜プログラング言語Idrisに入門させたい（v0.9）